from z3 import *
true_vm_code = [
	0xf5,#read(0,buf,0x20)
	0xf1,0xe1,0x0,0x0,0x0,0x0,#r1 = flag[0]
	0xf1,0xe2,0x1,0x0,0x0,0x0,#r2 = flag[1]
	0xf2,#r1 = 0x12^r1^r2
	0xf1,0xe4,0x0,0x0,0x0,0x0,#stack[0] = r1
	
	0xf1,0xe1,0x1,0x0,0x0,0x0,#r1 = flag[1]
	0xf1,0xe2,0x2,0x0,0x0,0x0,#r2 = flag[2]
	0xf2,#r1 = 0x12^r1^r2
	0xf1,0xe4,0x1,0x0,0x0,0x0,#stack[1] = r1
	
	0xf1,0xe1,0x2,0x0,0x0,0x0,#r1 = flag[2]
	0xf1,0xe2,0x3,0x0,0x0,0x0,#r2 = flag[3]
	0xf2,#r1 = 0x12^r1^r2
	0xf1,0xe4,0x2,0x0,0x0,0x0,#stack[2] = r1

	0xf1,0xe1,0x3,0x0,0x0,0x0,#r1 = flag[3]
	0xf1,0xe2,0x4,0x0,0x0,0x0,#r2 = flag[4]
	0xf2,#r1 = 0x12^r1^r2
	0xf1,0xe4,0x3,0x0,0x0,0x0,#stack[3] = r1

	0xf1,0xe1,0x4,0x0,0x0,0x0,#r1 = flag[4]
	0xf1,0xe2,0x5,0x0,0x0,0x0,#r2 = flag[5]
	0xf2,#r1 = 0x12^r1^r2
	0xf1,0xe4,0x4,0x0,0x0,0x0,#stack[4] = r1

	0xf1,0xe1,0x5,0x0,0x0,0x0,#r1 = flag[5]
	0xf1,0xe2,0x6,0x0,0x0,0x0,#r2 = flag[6]
	0xf2,#r1 = 0x12^r1^r2
	0xf1,0xe4,0x5,0x0,0x0,0x0,#stack[5] = r1

	0xf1,0xe1,0x6,0x0,0x0,0x0,#r1 = flag[6]
	0xf1,0xe2,0x7,0x0,0x0,0x0,#r2 = flag[7]
	0xf1,0xe3,0x8,0x0,0x0,0x0,#r3 = flag[8]
	0xf1,0xe5,0xC,0x0,0x0,0x0,#r4 = flag[12]
	0xf6, #r1 = (3*r1+2*r2+r3)
	0xf7, #r1 = r1*r4
	0xf1,0xe4,0x6,0x0,0x0,0x0,#stack[6] = r1

	0xf1,0xe1,0x7,0x0,0x0,0x0,#r1 = flag[7]
	0xf1,0xe2,0x8,0x0,0x0,0x0,#r2 = flag[8]
	0xf1,0xe3,0x9,0x0,0x0,0x0,#r3 = flag[9]
	0xf1,0xe5,0xC,0x0,0x0,0x0,#r4 = flag[12]
	0xf6, #r1 = (3*r1+2*r2+r3)
	0xf7, #r1 = r1*r4
	0xf1,0xe4,0x7,0x0,0x0,0x0,#stack[7] = r1

	0xf1,0xe1,0x8,0x0,0x0,0x0,#r1 = flag[8]
	0xf1,0xe2,0x9,0x0,0x0,0x0,#r2 = flag[9]
	0xf1,0xe3,0xA,0x0,0x0,0x0,#r3 = flag[10]
	0xf1,0xe5,0xC,0x0,0x0,0x0,#r4 = flag[12]
	0xf6, #r1 = (3*r1+2*r2+r3)
	0xf7, #r1 = r1*r4
	0xf1,0xe4,0x8,0x0,0x0,0x0,#stack[8] = r1

	0xf1,0xe1,0xD,0x0,0x0,0x0,#r1 = flag[13]
	0xf1,0xe2,0x13,0x0,0x0,0x0,#r2 = flag[19]
	0xf8,#r1 = r2,r2 = r1
	0xf1,0xe4,0xD,0x0,0x0,0x0,#stack[13] = r1
	0xf1,0xe7,0x13,0x0,0x0,0x0,#stack[19] = r2

	0xf1,0xe1,0xE,0x0,0x0,0x0,#r1 = flag[14]
	0xf1,0xe2,0x12,0x0,0x0,0x0,#r2 = flag[18]
	0xf8,#r1 = r2,r2 = r1
	0xf1,0xe4,0xE,0x0,0x0,0x0,#stack[14] = r1
	0xf1,0xe7,0x12,0x0,0x0,0x0,#stack[18] = r2

	0xf1,0xe1,0xF,0x0,0x0,0x0,#r1 = flag[15]
	0xf1,0xe2,0x11,0x0,0x0,0x0,#r2 = flag[17]
	0xf8,#r1 = r2,r2 = r1
	0xf1,0xe4,0xF,0x0,0x0,0x0,#stack[15] = r1
	0xf1,0xe7,0x11,0x0,0x0,0x0,#stack[17] = r2
	0xf4#ret
]

enc = [0x69, 0x45, 0x2a, 0x37, 0x9, 0x17, 0x6dc5, 0x5b0b, 0x705c, 0x72, 0x33, 0x76, 0x33, 0x21, 0x74, 0x31, 0x5f, 0x33, 0x73, 0x72]

a=Int('a')
b=Int('b')
c=Int('c')
solve((3*a+2*b+c)*0x33==0x6dc5,(3*b+2*c+0x72)*0x33==0x5b0b,(3*c+2*0x72+0x33)*0x33==0x705c)
#[c = 95, b = 51, a = 118]

flag = enc

flag[6] = 118
flag[7] = 51
flag[8] = 95

for i in range(6):
	flag[6-i-1] ^= flag[6-i]

def exchange(i,j):
	temp = flag[i]
	flag[i] = flag[j]
	flag[j] = temp

exchange(13,19)
exchange(14,18)
exchange(15,17)

string = ""
for i in flag:
	string += chr(i)
print string